注意：本課程為「IM3002 程式語言」的增補版本。已修過該門課並拿到學分的同學請勿修此門課。

講義、練習題等資訊請參考課程網頁： https://scm.iis.sinica.edu.tw/plfp/

本課程為「程式語言(Programming Languages)」系列課程之一，著眼點並不是教特定程式語言，而是以函數語言(functional language)為媒介，討論設計程式解決問題的思考方式、設計程式使用的數學與邏輯基礎、以及程式語言與形式符號在其中扮演的角色。其核心概念包括：

- 程式語言是一種形式語言，作為思考的工具。我們用程式語言表達概念，也用程式語言中的形式規則檢驗程式的正確性。

- 函數程設(functional programming)是一種相當簡化的程式設計模型。因為簡單，有更多易於掌握的性質，可作為討論程式語言的基礎。

- 有一整套程式設計理論奠基於歸納法(induction)之上。資料結構可用歸納法定義，其上的程式可用歸納寫成，關於該程式的性質也可用歸納法證明。與之相對的是餘歸納(coinduction).

- 上述兩種方法都不足以定義出所有程式 -- 為此我們將需要允許遞迴 (general recursion) 的模型. 然而，表達力變強大也意味著我們將失去一些好性質。

- 程式設計與定理證明是密切相關、相輔相成的活動。

- 函數語言這樣的簡單模型允許我們做等式推導，可作為一種程式設計方法 -- 將程式「算」出來。

- 好的型別系統常有「只要型別對，程式就會對」的特性。

- 型別系統與邏輯有密切關係：邏輯陳述相當於型別，具有該型別的程式則是該邏輯陳述的證明。

- 型別系統能幫助我們確立程式的正確性，甚至輔助我們寫程式。

- 更強大的型別系統相當於更具表達力的邏輯。同樣地，邏輯變強大的同時，我們也犧牲掉一些好掌握的性質。